:-op(500,fx,'incr').
:- static([ memory, sp, ar, dr, reg1, reg2, reg3, reg4, reg5 ]).

'$function' incr X	=  Z	:- Z is X + 1.

main :-
	init 
	&&
	*dr <= *reg3,
	*ar <= address3
	&&
	A = *ar,
	D = *dr,
	mem_write(A,D)
	&&
	X = *reg5,
	Y = incr( *reg4 ),
	Z = X \/ Y,
	*reg3 <= Z		% conflict exist at bus in trans itself
	&&
	*reg4 <= *reg3		% conflict exists (not connect)
	&&
	*reg1 <= *reg4,		% conflict exist  at bus in this subinterval
	*reg4 <= *reg5,
	*reg3 <= *reg2
	&&
	*reg2 <= *reg5 + *reg4	% facility lack
	&&
	R = *reg1,
	sub1(R)
	&& 
	Z = *reg4 ,
	sub1(Z)
	&& 
	X = *reg4,
	sub2(X),
	(
		*reg5 <= *reg3
		&&
		*reg2 <= *reg5
	)
	&&
	*ar <= address3
	&&
	A = *ar,
	mem_read(A,D),
	*dr <= D.

init :-
	length(1), *ar <= 0, *dr <= 0, *reg1 <= 1,
	*reg2 <= 2, *reg3 <= 3, *reg4 <= 4, *reg5 <= 5.

sub1(X) :-
	*reg2 <= X.

sub2(Y) :-
	sub3(Y)
	&&
	*reg1 <= Y. 		%  Y (imag_reg)  is return of state_call

sub3(Z) :-
	Z <- Z \/ *reg2.	%  Z (fin) is imag_reg

mem_read(Adr,Data) :- 
	!, Data = *memory(Adr), length(1).

mem_write(Adr,Data) :- 
	!, Adr1 <- Adr, *memory(Adr1) <= Data, length(1).


		fig. 1	sample program



path(reg1busA,[reg1,out],[busA,in]).
path(reg1busB,[reg1,out],[busB,in]).
path(busAreg1,[busA,out],[reg1,in]).
path(busBreg1,[busB,out],[reg1,in]).
.......
path(memobusA,[memory,out],[busA,in]).
path(busAmemi,[busA,out],[memory,in]).
path(regamema,[ar,out],[memory,address]).

func([conn,[bus,out],[bus,in]],[bus,conn]).
func([or,[or2,out],[or2,in1],[or2,in2]],[or2,cnt]).
func([incr,[inc,out],[inc,in]],[inc,cnt]).
func([set,register,[register,in]],[register,set]).
func([set,memory,[memory,in]],[memory,set]).

type(register,reg1).
type(register,reg2).
.......
type(memory,memory).
type(bus,busA).
type(bus,busB).
type(or2,or2A).
type(inc,incA).


		fig. 2	data path
